(declare-fun aTHySED_new () String)
(declare-fun shifted1_s () String)
(declare-fun shifted2_I0_6 () Int)
(declare-fun shifted2_PCTEMP_LHS_1 () String)
(declare-fun shifted2_PCTEMP_LHS_2 () Int)
(declare-fun shifted2_T0_6 () String)
(declare-fun shifted2_T1_5 () String)
(declare-fun shifted2_T1_6 () String)
(declare-fun shifted2_T2_5 () String)
(declare-fun shifted2_T2_6 () String)
(declare-fun shifted2_T3_6 () String)
(declare-fun shifted2_T4_6 () String)
(declare-fun shifted2_T5_6 () String)
(declare-fun shifted2_T_2 () String)
(declare-fun shifted2_T_SELECT_1 () Bool)
(assert (= "//%host%/gadgets/makeRequest" (str.replace aTHySED_new shifted1_s (str.at aTHySED_new (str.len aTHySED_new))) shifted2_PCTEMP_LHS_1))
(assert (= shifted2_T_SELECT_1 (not (= shifted2_PCTEMP_LHS_2 (- 1)))))
(assert (= shifted2_T_2 (str.++ shifted2_T1_5 shifted2_T2_5)))
(assert (= shifted2_T2_5 "?refresh=3600&url=http%3A%2F%2Fwww.mylisty.net%2FListy%2Fhtml%2FUserManager.action%3Ftype%3Dnew_user%26sid%3D0.6674028573006068&httpMethod=GET&headers=&postData=&authz=&st=&contentType=DOM&numEntries=3&getSummaries=false&signOwner=true&signViewer=true&gadget=http%3A%2F%2Fwww.mylisty.net%2FListy%2Fgadget%2FMyListy.xml&container=ig&bypassSpecCache=0"))
(assert (not (= shifted2_PCTEMP_LHS_2 0)))
(assert (and (= (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 2) (str.at shifted1_s 3)) (not (= (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 4) (str.at shifted1_s 5))) (= (str.at shifted1_s 3) (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 6)) (not (= (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 3) (str.at shifted1_s 5))) (not (= (str.at shifted1_s 3) (str.at shifted1_s 4))) (not (= (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 4) (str.at shifted1_s 6))) (not (= (str.at shifted1_s 4) (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 5))) (not (= (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 5) (str.at (str.substr aTHySED_new 0 (str.len shifted1_s)) 6))) (<= (str.len shifted1_s) 7) (= (str.len (str.substr aTHySED_new 0 (str.len shifted1_s))) 7) (not (= (str.len shifted1_s) 6)) (not (= (str.len shifted1_s) 5)) (> (str.len shifted1_s) 4) (not (= (str.len shifted1_s) 3)) (> (str.len shifted1_s) 2) (> (str.len shifted1_s) 0)))
(assert (ite shifted2_T_SELECT_1 (and (= shifted2_PCTEMP_LHS_2 shifted2_I0_6) (= shifted2_T_2 (str.++ shifted2_T0_6 shifted2_T1_6)) (= shifted2_I0_6 (str.len shifted2_T4_6)) (= 0 (str.len shifted2_T0_6)) (= shifted2_T1_6 (str.++ shifted2_T2_6 shifted2_T3_6)) (= shifted2_T2_6 (str.++ shifted2_T4_6 shifted2_T5_6)) (= shifted2_T5_6 "//") (not (str.in_re shifted2_T4_6 (re.++ (str.to_re "/") (str.to_re "/"))))) (and (= shifted2_T_2 (str.++ shifted2_T0_6 shifted2_T1_6)) (= 0 (str.len shifted2_T0_6)) (not (str.in_re shifted2_T1_6 (re.++ (str.to_re "/") (str.to_re "/")))))))
(assert (not (str.in_re shifted2_PCTEMP_LHS_1 (re.++ (str.to_re "%") (str.to_re "h") (str.to_re "o") (str.to_re "s") (str.to_re "t")))))
(check-sat)
